M1, M2:MsgA. M1 || M2  M2  M1  M2 

latex

Definitions	x:A. B(x), P  Q, M1  M2, M1  M2, P & Q, 1of(t), 2of(t), State(ds), Prop, Valtype(da;k), A & B, mk-ma, t  T, x. t(x), MsgA, M1 || M2, M1 ||decl M2, x(s)
Lemmas	fpf-sub-join-right, Id wf, id-deq wf, Knd wf, Kind-deq wf, fpf-cap wf, fpf-join wf, subtype-fpf2, subtype-fpf-cap-void, fpf-sub-join-left, ma-state wf, locl wf, top wf, subtype rel function, subtype rel dep function, subtype rel self, subtype-fpf-cap-top, pi1 wf, pi2 wf, product-deq wf, IdLnk wf, rcv wf, idlnk-deq wf, subtype rel list, subtype rel product, ma-compatible wf, msga wf